Complexité implicite
En informatique théorique, la complexité implicite est une branche de la théorie de la complexité calculatoire qui caractérise les classes de complexité par des restrictions syntaxiques sur le langage de programmation de haut niveau.
Définition[modifier | modifier le code]
La complexité implicite caractérise les classes de complexité par des restrictions syntaxiques sur le langage de programmation de haut niveau, souvent fonctionnel, logique ou par réécriture. Le programme qui résout un problème de la classe est donc écrit sans référence à une machine de bas niveau, alors que la théorie de la complexité classique se réfère à une machine de Turing.
Techniques[modifier | modifier le code]
La complexité implicite utilise des techniques de la théorie de la démonstration, des logiques sous-structurelles, de la théorie des modèles, de la théorie de la récursivité, de la réécriture et de la théorie des types.
Résultats et histoire[modifier | modifier le code]
Historiquement, les premiers concepts de complexité implicite sont le concept de fonction récursive (qui servira ensuite à définir la calculabilité par la thèse de Church) et le concept de fonction récursive primitive[1] (étudié par Rózsa Péter[2]). La réécriture terminant par l'ordre du multi-ensemble des chemins (MPO)[3] possède une longueur de dérivation dans cette classe.
Le théorème de Bellantoni et Cook montre que les fonctions en temps polynomial (FP) sont définies par la récursion sûre[4].
Sur base de ce résultat, on a défini la hiérarchie polynomiale[5] et la hiérarchie de comptage[6].
L'atelier DICE (Developments in Implicit Complexity)[7] est consacré à ce thème.
Notes et références[modifier | modifier le code]
- Hilbert, David, « Logic-Kalkül », Reprinted and translated in ' David Hilbert's Lectures on the Foundations of Arithmetic and Logic', (DOI 10.1007/978-3-540-69444-1_2)
- (hu) Rosza Péter, Recursive Functionen, Budapest, Akademiai Kiado,
- (en) D. Hofbauer, « Termination proofs with multiset path orderings imply primitive recursive derivation lengths », Theoretical Computer Science, , p. 129-140
- (en) Stephen J. Bellantoni et Stephen Cook, « A new recursion-theoretic characterization of the polytime functions », computational complexity, , p. 97–110 (ISSN 1016-3328, lire en ligne)
- (en) Isabel Oitavem, « The polynomial hierarchy of functions and its levels », Theoretical Computer Science, , p. 25-34 (DOI 10.1016/j.tcs.2021.11.016)
- (en) Ugo Dal Lago, Reinhard Kahle et Isabel Oitavem, « Implicit recursion-theoretic characterizations of counting classes », Arch. Math. Log. 61(7-8), , p. 1129-1144
- (en) Ugo Dal Lago, « Developments in Implicit Complexity (DICE 2012) », Theoretical Computer Science, (lire en ligne)
